A, B:Type, f:(AB), L1, L2:(A List). l_subset(A;L1;L2)  l_subset(B;map(f;L1);map(f;L2)) 

latex

Definitions	Type, t  T, x:AB(x), type List, x:A. B(x), (x  l), , P  Q, f(a), s = t, x:A  B(x), P & Q, x:A. B(x), map(f;as), x.A(x), P  Q, {T}, x. t(x), P  Q, l_subset(T;as;bs), A c B
Lemmas	all functionality wrt iff, implies functionality wrt iff, member map, map wf, l member wf